
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero</h1>
<div class="coq">
<br/>
<div class="doc">Translates contract logic to calculus </div>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html">ErgoSpec.Common.Types.ErgoType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html">ErgoSpec.ErgoNNRC.Lang.ErgoNNRC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html">ErgoSpec.Translation.ErgoNNRCtoJavaScript</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoNNRCtoJavaScriptCicero">ErgoNNRCtoJavaScriptCicero</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string_scope</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="accord_annotation">accord_annotation</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">clause_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">request_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">response_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">emit_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">state_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;"/**" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * <span class="id">Execute</span> <span class="id">the</span> <span class="id">smart</span> <span class="id">clause</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">param</span> {<span class="kwd">Context</span>} <span class="id">context</span> - <span class="id">the</span> <span class="id">Accord</span> <span class="id">context</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">param</span> {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#request_type">request_type</a></span> ++ "} <span class="id">context.request</span> - <span class="id">the</span> <span class="id">incoming</span> <span class="id">request</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">param</span> {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#response_type">response_type</a></span> ++ "} <span class="id">context.response</span> - <span class="id">the</span> <span class="id">response</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">param</span> {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#emit_type">emit_type</a></span> ++ "} <span class="id">context.emit</span> - <span class="id">the</span> <span class="id">emitted</span> <span class="id">events</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">param</span> {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#state_type">state_type</a></span> ++ "} <span class="id">context.state</span> - <span class="id">the</span> <span class="id">state</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#clause_name">clause_name</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#clause_init_name">clause_init_name</a></span> <span class="kwd">then</span> " * @<span class="id">AccordClauseLogicInit</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span> <span class="kwd">else</span> "")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " * @<span class="id">AccordClauseLogic</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ " */" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span>.<br/>
<br/>
<div class="doc">Note: this adjusts the external interface to that currently expected in Cicero. Namely:
<ul>
<li>
 This serialized/deserialized ErgoType objects to/from JSON
</li>
<li>
 This applies the result from the functional call to the call as effects to the input context
</li>
<li>
 This turns an error response into a JavaScript exception
</li>
</ul>
</div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="wrapper_function">wrapper_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fun_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">request_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">response_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">emit_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">state_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">clause_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">state_init</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#clause_name">clause_name</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#clause_init_name">clause_init_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"{ '$<span class="id">class</span>': '<span class="id">org.accordproject.cicero.contract.AccordContractState</span>', '<span class="id">stateId</span>' : '<span class="id">org.accordproject.cicero.contract.AccordContractState</span>#1' }"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">serializer.toJSON</span>(<span class="id">context.state</span>,{<span class="id">permitResourcesForRelationships</span>:<span class="id">true</span>})"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#accord_annotation">accord_annotation</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#clause_name">clause_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#request_type">request_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#response_type">response_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#emit_type">emit_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#state_type">state_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#quotel">quotel</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "<span class="id">function</span> " ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#fun_name">fun_name</a></span> ++ "(<span class="id">context</span>) {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  <span class="kwd">let</span> <span class="id">pcontext</span> = { '<span class="id">request</span>' : <span class="id">serializer.toJSON</span>(<span class="id">context.request</span>,{<span class="id">permitResourcesForRelationships</span>:<span class="id">true</span>}), '<span class="id">state</span>': " ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#state_init">state_init</a></span> ++ ", '<span class="id">contract</span>': <span class="id">serializer.toJSON</span>(<span class="id">context.contract</span>,{<span class="id">permitResourcesForRelationships</span>:<span class="id">true</span>}), '<span class="id">emit</span>': <span class="id">context.emit</span>, '<span class="id">now</span>': <span class="id">context.now</span>};" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  //<span class="id">logger.info</span>('<span class="id">ergo</span> <span class="id">context</span>: '+<span class="id">JSON.stringify</span>(<span class="id">pcontext</span>))" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  <span class="kwd">let</span> <span class="id">result</span> = <span class="id">new</span> " ++ <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span> ++ "()." ++ <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#clause_name">clause_name</a></span> ++ "(<span class="id">pcontext</span>);" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  <span class="kwd">if</span> (<span class="id">result.hasOwnProperty</span>('<span class="id">left</span>')) {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    //<span class="id">logger.info</span>('<span class="id">ergo</span> <span class="id">result</span>: '+<span class="id">JSON.stringify</span>(<span class="id">result</span>))" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="id">context.response</span> = <span class="id">serializer.fromJSON</span>(<span class="id">result.left.response</span>, {<span class="id">validate</span>: <span class="id">false</span>, <span class="id">acceptResourcesForRelationships</span>: <span class="id">true</span>},{<span class="id">permitResourcesForRelationships</span>:<span class="id">true</span>});" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="id">context.state</span> = <span class="id">serializer.fromJSON</span>(<span class="id">result.left.state</span>, {<span class="id">validate</span>: <span class="id">false</span>, <span class="id">acceptResourcesForRelationships</span>: <span class="id">true</span>});" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="kwd">let</span> <span class="id">emitResult</span> = [];" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="kwd">for</span> (<span class="kwd">let</span> <span class="id">i</span> = 0; <span class="id">i</span> &lt; <span class="id">result.left.emit.length</span>; <span class="id">i</span>++) {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "      <span class="id">emitResult.push</span>(<span class="id">serializer.fromJSON</span>(<span class="id">result.left.emit</span>[<span class="id">i</span>], {<span class="id">validate</span>: <span class="id">false</span>, <span class="id">acceptResourcesForRelationships</span>: <span class="id">true</span>}));" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    }" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="id">context.emit</span> = <span class="id">emitResult</span>;" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="kwd">return</span> <span class="id">context</span>;" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  } <span class="kwd">else</span> {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "    <span class="id">throw</span> <span class="id">new</span> <span class="id">Error</span>(<span class="id">result.right.message</span>);" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "  }" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "}" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="apply_wrapper_function">apply_wrapper_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_state_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">signature</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">clause_name</span>, <span class="id">request_type</span>, <span class="id">response_type</span>, <span class="id">emit_type</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#signature">signature</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fun_name</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span> ++ "<span class="id">_</span>" ++ <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id">clause_name</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#wrapper_function">wrapper_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#fun_name">fun_name</a></span> <span class="id">request_type</span> <span class="id">response_type</span> <span class="id">emit_type</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_state_type">contract_state_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span> <span class="id">clause_name</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#quotel">quotel</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="wrapper_functions">wrapper_functions</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">signatures</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">sig</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#apply_wrapper_function">apply_wrapper_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#signatures">signatures</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#sig">sig</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#quotel">quotel</a></span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#signatures">signatures</a></span>)).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_of_module_with_dispatch">javascript_of_module_with_dispatch</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">signatures</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_module">nnrc_module</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#preamble">preamble</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span>) ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#wrapper_functions">wrapper_functions</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#signatures">signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#quotel">quotel</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_of_declarations">javascript_of_declarations</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#modulen_declarations">modulen_declarations</a></span>) 0 0 <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#quotel">quotel</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#postamble">postamble</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#eol">eol</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="filter_signatures">filter_signatures</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">namespace</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sigs</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_signature">laergo_type_signature</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#sigs">sigs</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id">fname</span>,<span class="id">sig</span>) :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id">fname</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#clause_main_name">clause_main_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">params</span> := <span class="id">sig</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_params">type_signature_params</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">outtype</span> := <span class="id">sig</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_output">type_signature_output</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">emitstype</span> := <span class="id">sig</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_emits">type_signature_emits</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#params">params</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id">_</span>,<span class="id">reqtype</span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">reqtype</span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#outtype">outtype</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#emitstype">emitstype</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">reqname</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">outname</span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">emitsname</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fname</span>,<span class="id">reqname</span>,<span class="id">outname</span>,<span class="id">emitsname</span>) :: (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">reqname</span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">outname</span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">emitsname</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_emits_absolute_name">default_emits_absolute_name</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fname</span>,<span class="id">reqname</span>,<span class="id">outname</span>,<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#emitsname">emitsname</a></span>) :: (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span>, <span class="id">_</span>, <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> :: <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="filter_signatures_with_state">filter_signatures_with_state</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">namespace</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_state_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sigs</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ergo_type_signature">ergo_type_signature</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) * <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_state_type">contract_state_type</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#sigs">sigs</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_state_absolute_name">default_state_absolute_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">statename</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures">filter_signatures</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#namespace">namespace</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#sigs">sigs</a></span>, <span class="id">statename</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, "")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_module_to_javascript_cicero">ergoc_module_to_javascript_cicero</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">contract_state_type</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ergo_type">ergo_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sigs</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ergo_type_signature">ergo_type_signature</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_module">nnrc_module</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#javascript_of_module_with_dispatch">javascript_of_module_with_dispatch</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_name">contract_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#filter_signatures_with_state">filter_signatures_with_state</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#modulen_namespace">modulen_namespace</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#contract_state_type">contract_state_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#sigs">sigs</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#p">p</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_eol_newline">ErgoCodeGen.javascript_eol_newline</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_quotel_double">ErgoCodeGen.javascript_quotel_double</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScriptCicero.html#ErgoNNRCtoJavaScriptCicero">ErgoNNRCtoJavaScriptCicero</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
